i, a:Id, T:Type, P:(TProp).
@i: (with ds:  action a:T precondition a(v) is s,v. P(v) s v)  Dsys
& (D:Dsys.
& (@i: (with ds:  action a:T precondition a(v) is s,v. P(v) s v)  D
& ( D 
& ( realizes es.
& ( (e:E. loc(e) = i  Id  kind(e) = locl(a)  Knd  valtype(e)  T)
& ( & (e:E.
& ( & (loc(e) = i  Id
& ( & ( (kind(e) = locl(a)  Knd  P(val(e)))
& ( & ( & (e':E. (e <loc e')  e = e'  E & kind(e') = locl(a)  Knd  (v:T. P(v))))) 

latex

Definitions	t  T, P  Q, x:A. B(x), A & B, ES(the_w), E, s = t, (e <loc e'), left+right, f(a), Void, x:AB(x), Knd, x:AB(x), x:A. B(x), False, P  Q, A, 1of(t), loc(e), Id, Prop, locl(a), kind(e), valtype(e), P & Q, e@i. P(e), ee'.P(e'), @i Precondition for a(v)P State(ds) (v:T), PossibleWorld(D;w), FairFifo, World, D1  D2, Dsys, D realizes es. P(es), Type, x. t(x), State(ds), x(s), x.A(x),
Lemmas	s-pre-rule, ma-state wf, fpf-empty wf, dsys wf, d-sub wf, world wf, fair-fifo wf, possible-world wf, Knd wf, es-kind wf, locl wf, Id wf, es-loc wf, es-E wf, w-es wf